Search for: All records

Efficient real-time solvers for forward and inverse problems are essential in engineering and science applications. Machine learning surrogate models have emerged as promising alter- natives to traditional methods, offering substantially reduced computational time. Never- theless, these models typically demand extensive training datasets to achieve robust gen- eralization across diverse scenarios. While physics-based approaches can partially mitigate this data dependency and ensure physics-interpretable solutions, addressing scarce data regimes remains a challenge. Both purely data-driven and physics-based machine learning approaches demonstrate severe overfitting issues when trained with insufficient data. We propose a novel model-constrained Tikhonov autoencoder neural network framework, called TAEN, capable of learning both forward and inverse surrogate models using a single arbitrary observational sample. We develop comprehensive theoretical foundations including forward and inverse inference error bounds for the proposed approach for linear cases. For compara- tive analysis, we derive equivalent formulations for pure data-driven and model-constrained approach counterparts. At the heart of our approach is a data randomization strategy with theoretical justification, which functions as a generative mechanism for exploring the train- ing data space, enabling effective training of both forward and inverse surrogate models even with a single observation, while regularizing the learning process. We validate our approach through extensive numerical experiments on two challenging inverse problems: 2D heat conductivity inversion and initial condition reconstruction for time-dependent 2D Navier–Stokes equations. Results demonstrate that TAEN achieves accuracy comparable to traditional Tikhonov solvers and numerical forward solvers for both inverse and forward problems, respectively, while delivering orders of magnitude computational speedups. 

The rapidly growing online food delivery (OFD) market presents substantial logistical challenges for last-mile delivery operations. Sidewalk delivery robots (SDRs) have emerged as a promising alternative to on-demand workers, as these compact, box-sized robots efficiently deliver food or groceries over short distances via sidewalks. We propose a two-stage stochastic optimization model for a single-depot SDR system with integrated battery-swapping operations. In the first stage, a continuous approximation (CA) method determines the optimal fleet size and the required number of additional swappable batteries. The second-stage solutions are critical to facilitate the first-stage method. These involve solving a routing problem that incorporates battery-swapping decisions and penalties for late arrivals. To address this, we develop a customized heuristic based on adaptive large neighborhood search (ALNS) to generate high-quality solutions for the second stage. The fitted CA model integrates key factors, including time windows, battery swapping, and pickup-delivery orders. Numerical examples highlight the proposed approach’s efficiency in reducing computational time while maintaining solution accuracy. A case study and sensitivity analysis conducted on Purdue University’s campus illustrate the practical impacts of fleet size and the number of swappable batteries. 

Abstract Deep Neural Networks (DNNs) are increasingly deployed in critical applications, where ensuring their safety and robustness is paramount. We present$$_\text {CAV25}$$ ${}_{\mathrm{CAV}25}$, a high-performance DNN verification tool that uses the DPLL(T) framework and supports a wide-range of network architectures and activation functions. Since its debut in VNN-COMP’23, in which it achieved the New Participant Award and ranked 4th overall,$$_\text {CAV25}$$ ${}_{\mathrm{CAV}25}$has advanced significantly, achieving second place in VNN-COMP’24. This paper presents and evaluates the latest development of$$_\text {CAV25}$$ ${}_{\mathrm{CAV}25}$, focusing on the versatility, ease of use, and competitive performance of the tool.$$_\text {CAV25}$$ ${}_{\mathrm{CAV}25}$is available at:https://github.com/dynaroars/neuralsat. 

A refinement relation captures the state equivalence between two sequential circuits. It finds applications in various tasks of VLSI design automation, including regression verification, behavioral model synthesis, assertion synthesis, and design space exploration. However, manually constructing a refinement relation requires an engineer to have both domain knowledge and expertise in formal methods, which is especially challenging for complex designs after significant transformations. This paper presents a rigorous and efficient sequential equivalence checking algorithm for non-cycle-accurate designs. The algorithm can automatically find a concise and human-comprehensible refinement relation between two designs, helping engineers understand the essence of design transformations. We demonstrate the usefulness and efficiency of the proposed algorithm with experiments and case studies. In particular, we showcase how refinement relations can facilitate error detection and correction for LLM-generated RTL designs.